messed_calc - cr3 2024

計算に時間がかかるバイナリが与えられるので、最適化してくださいという問題

2つの処理で時間がかかっている

1. 64bitの乱数を取得し、その値がある条件を満たすまでループを回している

条件を満たす値は1つしかないので、終わらない

2. 0から、1の値までのforループを回して、何らかの計算をしている

2の結果の値からフラグが計算されているので、これを求められれば勝ち

1は条件式がわかっているので、z3で逆算する

code: solve1.py

from z3 import *

v12 = BitVec('v12', 64)

v20 = ~(v12 & 0xDE47307EBB83312A)

v18 = ~(v20 & v12)

v19 = ~(v20 & 0xDE47307EBB83312A)

s = Solver()

s.add(v19 & v18 == 0x42CAFCFA134CB9A8)

s.check()

m = s.model()

# 7165846561936668541

2は次のような関数

code: func.c

__int64 __fastcall `anonymous namespace'::OPTIMIZE_ME(_anonymous_namespace_ *this)

{

v3 = 0LL;

for ( i = 0LL; i < (__int64)this; ++i )

{

if ( (i & 1) != 0 )

{

if ( (i & 1) == 1 )

v3 -= i;

else

v3 = 0LL;

}

else

{

v3 += i;

}

}

return v3;

}

実験すると、以下の値を返す関数だとわかる

あとはこの値からフラグの文字列を計算する

が、うまくいかなかったのでマイナスを付けたらそれっぽい文字列がでてきた

code: solve.py

v = -3582923280968334270

print(int.to_bytes(rol(v, 20, 64) ^ 0x104C720B3B3F960D, 8, 'little'))

print(int.to_bytes(rol(v, 6, 64) ^ 0xEC98E4A44683346C, 8, 'little'))

# b'cr\x13\x7fw4it'

# b'\xdf$r_1t!}'

code: test.py

print(round(7165846561936668541 / 2)) # 3582923280968334336

print(7165846561936668541 // 2) # 3582923280968334270